* Step 1: Bounds WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
U11(mark(X1),X2) -> mark(U11(X1,X2))
U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(zeros()) -> mark(cons(0(),zeros()))
and(mark(X1),X2) -> mark(and(X1,X2))
and(ok(X1),ok(X2)) -> ok(and(X1,X2))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
isNat(ok(X)) -> ok(isNat(X))
isNatIList(ok(X)) -> ok(isNatIList(X))
isNatList(ok(X)) -> ok(isNatList(X))
length(mark(X)) -> mark(length(X))
length(ok(X)) -> ok(length(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(nil()) -> ok(nil())
proper(tt()) -> ok(tt())
proper(zeros()) -> ok(zeros())
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
- Signature:
{U11/2,active/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,proper/1,s/1,top/1} / {0/0,mark/1
,nil/0,ok/1,tt/0,zeros/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,active,and,cons,isNat,isNatIList,isNatList,length,proper,s
,top} and constructors {0,mark,nil,ok,tt,zeros}
+ Applied Processor:
Bounds {initialAutomaton = perSymbol, enrichment = match}
+ Details:
The problem is match-bounded by 5.
The enriched problem is compatible with follwoing automaton.
0_0() -> 1
0_1() -> 20
0_2() -> 32
0_3() -> 43
U11_0(1,1) -> 2
U11_0(1,10) -> 2
U11_0(1,11) -> 2
U11_0(1,12) -> 2
U11_0(1,16) -> 2
U11_0(1,17) -> 2
U11_0(10,1) -> 2
U11_0(10,10) -> 2
U11_0(10,11) -> 2
U11_0(10,12) -> 2
U11_0(10,16) -> 2
U11_0(10,17) -> 2
U11_0(11,1) -> 2
U11_0(11,10) -> 2
U11_0(11,11) -> 2
U11_0(11,12) -> 2
U11_0(11,16) -> 2
U11_0(11,17) -> 2
U11_0(12,1) -> 2
U11_0(12,10) -> 2
U11_0(12,11) -> 2
U11_0(12,12) -> 2
U11_0(12,16) -> 2
U11_0(12,17) -> 2
U11_0(16,1) -> 2
U11_0(16,10) -> 2
U11_0(16,11) -> 2
U11_0(16,12) -> 2
U11_0(16,16) -> 2
U11_0(16,17) -> 2
U11_0(17,1) -> 2
U11_0(17,10) -> 2
U11_0(17,11) -> 2
U11_0(17,12) -> 2
U11_0(17,16) -> 2
U11_0(17,17) -> 2
U11_1(1,1) -> 18
U11_1(1,10) -> 18
U11_1(1,11) -> 18
U11_1(1,12) -> 18
U11_1(1,16) -> 18
U11_1(1,17) -> 18
U11_1(10,1) -> 18
U11_1(10,10) -> 18
U11_1(10,11) -> 18
U11_1(10,12) -> 18
U11_1(10,16) -> 18
U11_1(10,17) -> 18
U11_1(11,1) -> 18
U11_1(11,10) -> 18
U11_1(11,11) -> 18
U11_1(11,12) -> 18
U11_1(11,16) -> 18
U11_1(11,17) -> 18
U11_1(12,1) -> 18
U11_1(12,10) -> 18
U11_1(12,11) -> 18
U11_1(12,12) -> 18
U11_1(12,16) -> 18
U11_1(12,17) -> 18
U11_1(16,1) -> 18
U11_1(16,10) -> 18
U11_1(16,11) -> 18
U11_1(16,12) -> 18
U11_1(16,16) -> 18
U11_1(16,17) -> 18
U11_1(17,1) -> 18
U11_1(17,10) -> 18
U11_1(17,11) -> 18
U11_1(17,12) -> 18
U11_1(17,16) -> 18
U11_1(17,17) -> 18
active_0(1) -> 3
active_0(10) -> 3
active_0(11) -> 3
active_0(12) -> 3
active_0(16) -> 3
active_0(17) -> 3
active_1(1) -> 29
active_1(10) -> 29
active_1(11) -> 29
active_1(12) -> 29
active_1(16) -> 29
active_1(17) -> 29
active_2(20) -> 30
active_2(21) -> 30
active_3(38) -> 37
active_4(32) -> 42
active_4(36) -> 42
active_4(44) -> 45
active_5(43) -> 46
and_0(1,1) -> 4
and_0(1,10) -> 4
and_0(1,11) -> 4
and_0(1,12) -> 4
and_0(1,16) -> 4
and_0(1,17) -> 4
and_0(10,1) -> 4
and_0(10,10) -> 4
and_0(10,11) -> 4
and_0(10,12) -> 4
and_0(10,16) -> 4
and_0(10,17) -> 4
and_0(11,1) -> 4
and_0(11,10) -> 4
and_0(11,11) -> 4
and_0(11,12) -> 4
and_0(11,16) -> 4
and_0(11,17) -> 4
and_0(12,1) -> 4
and_0(12,10) -> 4
and_0(12,11) -> 4
and_0(12,12) -> 4
and_0(12,16) -> 4
and_0(12,17) -> 4
and_0(16,1) -> 4
and_0(16,10) -> 4
and_0(16,11) -> 4
and_0(16,12) -> 4
and_0(16,16) -> 4
and_0(16,17) -> 4
and_0(17,1) -> 4
and_0(17,10) -> 4
and_0(17,11) -> 4
and_0(17,12) -> 4
and_0(17,16) -> 4
and_0(17,17) -> 4
and_1(1,1) -> 22
and_1(1,10) -> 22
and_1(1,11) -> 22
and_1(1,12) -> 22
and_1(1,16) -> 22
and_1(1,17) -> 22
and_1(10,1) -> 22
and_1(10,10) -> 22
and_1(10,11) -> 22
and_1(10,12) -> 22
and_1(10,16) -> 22
and_1(10,17) -> 22
and_1(11,1) -> 22
and_1(11,10) -> 22
and_1(11,11) -> 22
and_1(11,12) -> 22
and_1(11,16) -> 22
and_1(11,17) -> 22
and_1(12,1) -> 22
and_1(12,10) -> 22
and_1(12,11) -> 22
and_1(12,12) -> 22
and_1(12,16) -> 22
and_1(12,17) -> 22
and_1(16,1) -> 22
and_1(16,10) -> 22
and_1(16,11) -> 22
and_1(16,12) -> 22
and_1(16,16) -> 22
and_1(16,17) -> 22
and_1(17,1) -> 22
and_1(17,10) -> 22
and_1(17,11) -> 22
and_1(17,12) -> 22
and_1(17,16) -> 22
and_1(17,17) -> 22
cons_0(1,1) -> 5
cons_0(1,10) -> 5
cons_0(1,11) -> 5
cons_0(1,12) -> 5
cons_0(1,16) -> 5
cons_0(1,17) -> 5
cons_0(10,1) -> 5
cons_0(10,10) -> 5
cons_0(10,11) -> 5
cons_0(10,12) -> 5
cons_0(10,16) -> 5
cons_0(10,17) -> 5
cons_0(11,1) -> 5
cons_0(11,10) -> 5
cons_0(11,11) -> 5
cons_0(11,12) -> 5
cons_0(11,16) -> 5
cons_0(11,17) -> 5
cons_0(12,1) -> 5
cons_0(12,10) -> 5
cons_0(12,11) -> 5
cons_0(12,12) -> 5
cons_0(12,16) -> 5
cons_0(12,17) -> 5
cons_0(16,1) -> 5
cons_0(16,10) -> 5
cons_0(16,11) -> 5
cons_0(16,12) -> 5
cons_0(16,16) -> 5
cons_0(16,17) -> 5
cons_0(17,1) -> 5
cons_0(17,10) -> 5
cons_0(17,11) -> 5
cons_0(17,12) -> 5
cons_0(17,16) -> 5
cons_0(17,17) -> 5
cons_1(1,1) -> 23
cons_1(1,10) -> 23
cons_1(1,11) -> 23
cons_1(1,12) -> 23
cons_1(1,16) -> 23
cons_1(1,17) -> 23
cons_1(10,1) -> 23
cons_1(10,10) -> 23
cons_1(10,11) -> 23
cons_1(10,12) -> 23
cons_1(10,16) -> 23
cons_1(10,17) -> 23
cons_1(11,1) -> 23
cons_1(11,10) -> 23
cons_1(11,11) -> 23
cons_1(11,12) -> 23
cons_1(11,16) -> 23
cons_1(11,17) -> 23
cons_1(12,1) -> 23
cons_1(12,10) -> 23
cons_1(12,11) -> 23
cons_1(12,12) -> 23
cons_1(12,16) -> 23
cons_1(12,17) -> 23
cons_1(16,1) -> 23
cons_1(16,10) -> 23
cons_1(16,11) -> 23
cons_1(16,12) -> 23
cons_1(16,16) -> 23
cons_1(16,17) -> 23
cons_1(17,1) -> 23
cons_1(17,10) -> 23
cons_1(17,11) -> 23
cons_1(17,12) -> 23
cons_1(17,16) -> 23
cons_1(17,17) -> 23
cons_1(20,21) -> 19
cons_2(32,33) -> 31
cons_2(34,35) -> 30
cons_3(32,33) -> 38
cons_3(36,33) -> 38
cons_3(39,40) -> 37
cons_4(42,33) -> 37
cons_4(43,41) -> 44
cons_5(46,41) -> 45
isNat_0(1) -> 6
isNat_0(10) -> 6
isNat_0(11) -> 6
isNat_0(12) -> 6
isNat_0(16) -> 6
isNat_0(17) -> 6
isNat_1(1) -> 24
isNat_1(10) -> 24
isNat_1(11) -> 24
isNat_1(12) -> 24
isNat_1(16) -> 24
isNat_1(17) -> 24
isNatIList_0(1) -> 7
isNatIList_0(10) -> 7
isNatIList_0(11) -> 7
isNatIList_0(12) -> 7
isNatIList_0(16) -> 7
isNatIList_0(17) -> 7
isNatIList_1(1) -> 25
isNatIList_1(10) -> 25
isNatIList_1(11) -> 25
isNatIList_1(12) -> 25
isNatIList_1(16) -> 25
isNatIList_1(17) -> 25
isNatList_0(1) -> 8
isNatList_0(10) -> 8
isNatList_0(11) -> 8
isNatList_0(12) -> 8
isNatList_0(16) -> 8
isNatList_0(17) -> 8
isNatList_1(1) -> 26
isNatList_1(10) -> 26
isNatList_1(11) -> 26
isNatList_1(12) -> 26
isNatList_1(16) -> 26
isNatList_1(17) -> 26
length_0(1) -> 9
length_0(10) -> 9
length_0(11) -> 9
length_0(12) -> 9
length_0(16) -> 9
length_0(17) -> 9
length_1(1) -> 27
length_1(10) -> 27
length_1(11) -> 27
length_1(12) -> 27
length_1(16) -> 27
length_1(17) -> 27
mark_0(1) -> 10
mark_0(10) -> 10
mark_0(11) -> 10
mark_0(12) -> 10
mark_0(16) -> 10
mark_0(17) -> 10
mark_1(18) -> 2
mark_1(18) -> 18
mark_1(19) -> 3
mark_1(19) -> 29
mark_1(22) -> 4
mark_1(22) -> 22
mark_1(23) -> 5
mark_1(23) -> 23
mark_1(27) -> 9
mark_1(27) -> 27
mark_1(28) -> 14
mark_1(28) -> 28
mark_2(31) -> 30
nil_0() -> 11
nil_1() -> 20
nil_2() -> 36
ok_0(1) -> 12
ok_0(10) -> 12
ok_0(11) -> 12
ok_0(12) -> 12
ok_0(16) -> 12
ok_0(17) -> 12
ok_1(18) -> 2
ok_1(18) -> 18
ok_1(20) -> 13
ok_1(20) -> 29
ok_1(21) -> 13
ok_1(21) -> 29
ok_1(22) -> 4
ok_1(22) -> 22
ok_1(23) -> 5
ok_1(23) -> 23
ok_1(24) -> 6
ok_1(24) -> 24
ok_1(25) -> 7
ok_1(25) -> 25
ok_1(26) -> 8
ok_1(26) -> 26
ok_1(27) -> 9
ok_1(27) -> 27
ok_1(28) -> 14
ok_1(28) -> 28
ok_2(32) -> 34
ok_2(33) -> 35
ok_2(36) -> 34
ok_3(38) -> 30
ok_3(41) -> 40
ok_3(43) -> 39
ok_4(44) -> 37
proper_0(1) -> 13
proper_0(10) -> 13
proper_0(11) -> 13
proper_0(12) -> 13
proper_0(16) -> 13
proper_0(17) -> 13
proper_1(1) -> 29
proper_1(10) -> 29
proper_1(11) -> 29
proper_1(12) -> 29
proper_1(16) -> 29
proper_1(17) -> 29
proper_2(19) -> 30
proper_2(20) -> 34
proper_2(21) -> 35
proper_3(31) -> 37
proper_3(32) -> 39
proper_3(33) -> 40
s_0(1) -> 14
s_0(10) -> 14
s_0(11) -> 14
s_0(12) -> 14
s_0(16) -> 14
s_0(17) -> 14
s_1(1) -> 28
s_1(10) -> 28
s_1(11) -> 28
s_1(12) -> 28
s_1(16) -> 28
s_1(17) -> 28
top_0(1) -> 15
top_0(10) -> 15
top_0(11) -> 15
top_0(12) -> 15
top_0(16) -> 15
top_0(17) -> 15
top_1(29) -> 15
top_2(30) -> 15
top_3(37) -> 15
top_4(45) -> 15
tt_0() -> 16
tt_1() -> 20
tt_2() -> 36
zeros_0() -> 17
zeros_1() -> 21
zeros_2() -> 33
zeros_3() -> 41
* Step 2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
U11(mark(X1),X2) -> mark(U11(X1,X2))
U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(zeros()) -> mark(cons(0(),zeros()))
and(mark(X1),X2) -> mark(and(X1,X2))
and(ok(X1),ok(X2)) -> ok(and(X1,X2))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
isNat(ok(X)) -> ok(isNat(X))
isNatIList(ok(X)) -> ok(isNatIList(X))
isNatList(ok(X)) -> ok(isNatList(X))
length(mark(X)) -> mark(length(X))
length(ok(X)) -> ok(length(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(nil()) -> ok(nil())
proper(tt()) -> ok(tt())
proper(zeros()) -> ok(zeros())
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
- Signature:
{U11/2,active/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,proper/1,s/1,top/1} / {0/0,mark/1
,nil/0,ok/1,tt/0,zeros/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,active,and,cons,isNat,isNatIList,isNatList,length,proper,s
,top} and constructors {0,mark,nil,ok,tt,zeros}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))